;;;===========================================================================
;;;
;;; Cone construction (Second Version)
;;;
;;;---------------------------------------------------------------------------
;;;
;;; JHV 
;;;
;;; Start date: 25/05/10 || End date: 26/05/10
;;;
;;;===========================================================================


(in-package "ACL2")

(include-book "algebraic-data-structures")

(encapsulate
 
 ;;**************************************************
 ;; Signaturas
 ;;**************************************************

 (
 ;;--------------------------------------------------
 ;; The signatures of the ring R
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-ring *) => *)
 ;; Addition operation ring
 ((addition-ring * *)=> *)
 ;; Product operation ring
 ((product-ring * *) => *)
 ;; Inverse ring
 ((inverse *) => *)
 ;; Zero element ring
 ((zero-element ) => *)
 ;; Unit element ring
 ((unit )=> *)

 ;;--------------------------------------------------
 ;; D Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-D * *) => *)
 ;; Group Operation 
 ((group-operation-D * * *) => *)
 ;; Zero element
 ((zero-D *) => *)
 ;; External multiplication
 ((external-D * * *) => *)
 ;; Inverse element
 ((inverse-D * *) => *)

 ;;--------------------------------------------------
 ;; The D differential 
 ;;--------------------------------------------------

 ;; The differential
 ((d-D * *) => *)
 


 ;;--------------------------------------------------
 ;; C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 ((inv-C * *) => *)
 ;; Group Operation 
 ((group-operation-C * * *) => *)
 ;; Zero element
 ((zero-C *) => *)
 ;; External multiplication
 ((external-C * * *) => *)
 ;; Inverse element
 ((inverse-C * *) => *)

 ;;--------------------------------------------------
 ;; The C differential
 ;;--------------------------------------------------

 ;; The differential
 ((d-C * *) => *)
 
 
 ;;--------------------------------------------------
 ;; The morphism
 ;;--------------------------------------------------

 ;; The function
 ((phi * *) => *)
 

 
 )
 ;;**************************************************
 ;; Witnesses
 ;;**************************************************
 
 ;;--------------------------------------------------
 ;; The witnesses of the ring Z
 ;;--------------------------------------------------

 ;; The characteristic function

 (local (defun inv-ring (a)
	  (integerp a)))
 
 ;; Addition operation Z
 (local (defun addition-ring (a b)
	  (+ a b)))

 ;; Product operation ring
 (local (defun product-ring (a b)
	  (* a b)))

 ;; Inverse addition
 (local (defun inverse (a)
	  (- a)))

 ;; Zero element ring
 (local (defun zero-element nil
	  0))

 ;; Unit element ring
 (local (defun unit nil
	  1))

 ;;--------------------------------------------------
 ;; D Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-D (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-D (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-D (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-D (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse element
 (local (defun inverse-D (n a)
	  (declare (ignore n a))
	  0))


 ;;--------------------------------------------------
 ;; The D differential 
 ;;--------------------------------------------------

 ;; The differential
 (local (defun d-D (n a)
	  (declare (ignore n a))
	  0))

 

 ;;--------------------------------------------------
 ;; C Chain Complex (A R-Module)
 ;;--------------------------------------------------

 ;; Characteristic function
 (local (defun inv-C (n a) 
	  (declare (ignore n))
	  (equal a 0)))

 ;; Group Operation 
 (local (defun group-operation-C (n a b)
	  (declare (ignore n))
	  (+ a b)))

 ;; Zero element
 (local (defun zero-C (n)
	  (declare (ignore n))
	  0))

 ;; External multiplication
 (local (defun external-C (n a b)
	  (declare (ignore n))
	  (* a b)))

 ;; Inverse C
 (local (defun inverse-C (n a)
	  (declare (ignore n a))
	  0))

 


 ;;--------------------------------------------------
 ;; The C differential
 ;;--------------------------------------------------
 
  ;; The differential
 (local (defun d-C (n a)
	  (declare (ignore n a))
	  0))



 ;;--------------------------------------------------
 ;; The morphism
 ;;--------------------------------------------------

 ;; The function
 (local (defun phi (n a)
	  (declare (ignore n a))
	  0))


  ;;************************************************** 
  ;; Properties
  ;;************************************************** 
  


(check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring :addition-ring 'addition-ring :zero-element 'zero-element
		    :inverse 'inverse :product-ring 'product-ring :unit 'unit
		    :inv-cc 'inv-c :group-operation-cc 'group-operation-c :zero-cc 'zero-c :external-cc 'external-c
		    :inverse-cc 'inverse-c :d-cc 'd-c)
 'C)


(check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring :addition-ring 'addition-ring :zero-element 'zero-element
		    :inverse 'inverse :product-ring 'product-ring :unit 'unit
		    :inv-cc 'inv-d :group-operation-cc 'group-operation-d :zero-cc 'zero-d :external-cc 'external-d
		    :inverse-cc 'inverse-d :d-cc 'd-d)
 'D)

 ;;--------------------------------------------------
 ;; Properties of the morphism
 ;;--------------------------------------------------

  ;; phi is a morphism
(check-chain-complex-morphism-degree-0-p
(chain-complex-morphism-degree-0 
 (chain-complex 'inv-ring 'addition-ring 'zero-element 'inverse 'product-ring 'unit 'inv-D 'group-operation-D 'zero-D 'external-D 'inverse-D 'd-D )
 (chain-complex 'inv-ring 'addition-ring 'zero-element 'inverse 'product-ring 'unit 'inv-C 'group-operation-C 'zero-C 'external-C 'inverse-C 'd-C )
 'phi) 'phi)

)


;;==================================================
;; The Cone definitions
;;==================================================


 ;;--------------------------------------------------
 ;; Cone Chain Complex 
 ;;--------------------------------------------------

 ;; Characteristic function
(defun inv-cone (n a) 
  (and (equal (list (car a) (cadr a)) a)
       (inv-C (1+ n) (car a))
       (inv-D n (cadr a))     
       )
  )

 ;; Group Operation 
(defun group-operation-cone (n a b)
   (list (group-operation-C (1+ n) (car a) (car b))
	 (group-operation-D n (cadr a) (cadr b))))
	  

 ;; Zero element
(defun zero-cone (n)
   (list (zero-C (1+ n))
	 (zero-D n)))
   

 ;; External multiplication
(defun external-cone (n a b)
   (list (external-C (1+ n) a (car b))
	 (external-D n a (cadr b)))
	 )

 ;; Inverse element
(defun inverse-cone (n a)
   (list (inverse-C (1+ n) (car a))
	 (inverse-D n (cadr a)))
   )
	 

 ;;--------------------------------------------------
 ;; Cone differential 
 ;;--------------------------------------------------

 ;; The differential
(defun d-cone (n a)
  (list (group-operation-C n (d-C (1+ n) (car a)) (phi n (cadr a)))
	(inverse-D (1- n) (d-D n (cadr a)))) 
	  )


 ;;--------------------------------------------------
 ;; The Cone is a Chain Complex 
 ;;--------------------------------------------------

(encapsulate
 ()

(defthm group-operation-C-distrivutivity
  (implies (and (inv-c n a)
		(inv-c n b)
		(inv-c n c)
		(integerp n))
	   (equal (group-operation-c n a (group-operation-c n b c))
		  (group-operation-c n c (group-operation-c n a b))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance |C-is-a-chain-complex|)))))

(defthm group-operation-D-distrivutivity
  (implies (and (inv-d n a)
		(inv-d n b)
		(inv-d n c)
		(integerp n))
	   (equal (group-operation-d n a (group-operation-d n b c))
		  (group-operation-d n c (group-operation-d n a b))
		  ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance |D-is-a-chain-complex|)))))


(local (defthm inv-d-c
  (implies (and (inv-c n a) (integerp n))
	   (inv-c (1- n) (d-c n a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance |C-is-a-chain-complex|))))))

(local (defthm -1+1+n=n
	 (implies (integerp n)
		  (equal (1- (+ 1 n)) n))
	 :rule-classes nil))

(local (defthm inv-d-c-2
  (implies (and (inv-c (+ 1 n) (car a)) (integerp n))
	   (inv-c (1- (+ 1 n)) (d-c (+ 1 n) (car a))))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance inv-d-c
			    (n (+ 1 n))
			    (a (car a)))
		 )))))


(defthm inv-d-c-3
  (implies (and (inv-c (+ 1 n) (car a)) (integerp n))
	   (inv-c n (d-c (+ 1 n) (car a))))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance -1+1+n=n)
		 (:instance inv-d-c-2)
		 ))))


(local (defthm inv-phi
  (implies (and (inv-d n a) (integerp n))
	   (inv-c n (phi n a)))))


(defthm inv-phi-2
  (implies (and (inv-d n (cadr a)) (integerp n))
	   (inv-c n (phi n (cadr a)))))


(defthm inv-group-operation-c
  (implies (and (inv-c n a)
		(inv-c n b)
		(integerp n))
	   (inv-c n (group-operation-c n a b))))

(defthm inv-group-operation-c-2
  (implies (and (inv-c (1+ n) (car a))
		(inv-d n (cadr a))
		(integerp n))
	   (inv-c n (group-operation-c n 
				       (phi n (cadr a))
				       (d-c (1+ n) (car a))
					      )))
  :hints (("Goal" :use ((:instance inv-d-c-3)
			(:instance inv-phi-2)
			(:instance inv-group-operation-c
				   (a (phi n (cadr a)))
				   (b (d-c (1+ n) (car a))))))))


(local (defthm +1-1+n=n
	 (implies (integerp n)
		  (equal (+ 1 -1 N)
			 n))
	 :rule-classes nil))


(defthm inv-group-operation-c-3
  (implies (and (inv-c (1+ n) (car a))
		(inv-d n (cadr a))
		(integerp n))
	   (inv-c (+ 1 -1 N) (group-operation-c n 
				       (phi n (cadr a))
				       (d-c (1+ n) (car a))
					      )))
  :hints (("Goal" :use ((:instance |+1-1+N=N|)
			(:instance inv-group-operation-c-2)))))
	   

(local (defthm inv-d-d
  (implies (and (inv-d n a) (integerp n))
	   (inv-d (+ n -1) (d-d n a)))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance |D-is-a-chain-complex|))))))

(defthm inv-d-d-2
  (implies (and (inv-d n (cadr a)) (integerp n))
	   (inv-d (+ -1 n) (d-d n (cadr a))))
   :hints (("Goal" :do-not-induct t
	   :use ((:instance inv-d-d (a (cadr a)))))))


(local (defthm group-operation-C-commutativity
  (implies (and (inv-c n a)
		(inv-c n b)
		(integerp n))
	   (equal (group-operation-c n a b)
		  (group-operation-c n b a)))
  ))

(local (defthm group-operation-C-distrivutivity-3
  (implies (and (inv-c n a)
		(inv-c n b)
		(inv-c n c)
		(integerp n))
	   (equal (group-operation-c n a (group-operation-c n b c))
		  (group-operation-c n b (group-operation-c n a c))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance group-operation-C-commutativity
			    (a b) (b c))
		 (:instance group-operation-C-distrivutivity
			    (c b) (b c)))))))


(local(defthm group-operation-C-distrivutivity-4
  (implies (and (inv-c n a)
		(inv-c n b)
		(inv-c n c)
		(inv-c n d)
		(integerp n))
	   (equal (group-operation-c n 
				     (group-operation-c n a b)
				     (group-operation-c n c d))
		  (group-operation-c n 
				     (group-operation-c n c a)
				     (group-operation-c n d b))))))


(defthm group-operation-group-operation-C
  (implies (and (inv-d n (cadr a))
		(inv-d n (cadr b))
		(inv-c (+ 1 n) (car a))
		(inv-c (+ 1 n) (car b))
		(integerp n))
	   (equal (GROUP-OPERATION-C N
                               (GROUP-OPERATION-C n
                                                  (D-C (+ 1 N) (CAR A))
                                                  (D-C (+ 1 N) (CAR B)))
                               (GROUP-OPERATION-C N (PHI N (CADR A))
                                                  (PHI N (CADR B))))
		  (GROUP-OPERATION-C n
                               (GROUP-OPERATION-C N (PHI N (CADR A))
                                                  (D-C (+ 1 N) (CAR A)))
                               (GROUP-OPERATION-C N (PHI N (CADR B))
                                                  (D-C (+ 1 N) (CAR B))))))
  :hints (("Goal" :use ((:instance inv-phi-2 (a a))
			(:instance inv-phi-2 (a b))
			(:instance inv-d-c-3 (a a))
			(:instance inv-d-c-3 (a b))
			(:instance group-operation-C-distrivutivity-4
				   (a (D-C (+ 1 N) (CAR A)))
				   (b (D-C (+ 1 N) (CAR B)))
				   (c (PHI N (CADR A)))
				   (d (PHI N (CADR B))))))))


(defthm group-operation-group-operation-C-b
  (implies (and (inv-d n (cadr a))
		(inv-d n (cadr b))
		(inv-c (+ 1 n) (car a))
		(inv-c (+ 1 n) (car b))
		(integerp n))
	   (equal (GROUP-OPERATION-C N
                               (GROUP-OPERATION-C (+ -1 1 N)
                                                  (D-C (+ 1 N) (CAR A))
                                                  (D-C (+ 1 N) (CAR B)))
                               (GROUP-OPERATION-C N (PHI N (CADR A))
                                                  (PHI N (CADR B))))
		  (GROUP-OPERATION-C (+ 1 -1 N)
                               (GROUP-OPERATION-C N (PHI N (CADR A))
                                                  (D-C (+ 1 N) (CAR A)))
                               (GROUP-OPERATION-C N (PHI N (CADR B))
                                                  (D-C (+ 1 N) (CAR B))))))
  :hints (("Goal" :use ((:instance -1+1+n=n)
			(:instance |+1-1+N=N|)
			(:instance group-operation-group-operation-C)))))



(local (defthm group-operation-external
	 (implies (and (inv-c n a)
		       (inv-c n b)
		       (inv-ring r)
		       (integerp n))
		  (equal (group-operation-c n
					    (external-c n r a)
					    (external-c n r b))
			 (external-c n r (group-operation-c n b a))))))



(local (defthm group-operation-external-b
  (implies (and (inv-d n (cadr a))
		(inv-c (+ 1 n) (car a))
		(inv-ring r)
		(integerp n))
	   (EQUAL (GROUP-OPERATION-C N
                                   (EXTERNAL-C n
                                               R (D-C (+ 1 N) (CAR A)))
                                   (EXTERNAL-C N R (PHI N (CADR A))))
                (EXTERNAL-C n
                            R
                            (GROUP-OPERATION-C N (PHI N (CADR A))
                                               (D-C (+ 1 N) (CAR A))))))
   :hints (("Goal" 
	    :use ((:instance inv-phi-2 (a a))
			 (:instance inv-d-c-3 (a a))
			 (:instance group-operation-external
				   (a (D-C (+ 1 N) (CAR A)))
				   (b (PHI N (CADR A)))))))))


(defthm group-operation-external-b-2
  (implies (and (inv-d n (cadr a))
		(inv-c (+ 1 n) (car a))
		(inv-ring r)
		(integerp n))
	   (EQUAL (GROUP-OPERATION-C N
                                   (EXTERNAL-C (+ -1 1 N)
                                               R (D-C (+ 1 N) (CAR A)))
                                   (EXTERNAL-C N R (PHI N (CADR A))))
                (EXTERNAL-C (+ 1 -1 N)
                            R
                            (GROUP-OPERATION-C N (PHI N (CADR A))
                                               (D-C (+ 1 N) (CAR A))))))
   :hints (("Goal" :in-theory (disable GROUP-OPERATION-EXTERNAL)
	    :use ((:instance -1+1+n=n)
			(:instance |+1-1+N=N|)
			(:instance group-operation-external-b)))))

  
(defthm group-operation-zero-zero
  (implies (integerp n)
	   (EQUAL (GROUP-OPERATION-C N (ZERO-C (+ -1 1 N))
                                   (ZERO-C N))
                (ZERO-C (+ 1 -1 N))))
  :hints (("Goal" 
	   :use ((:instance -1+1+n=n)
			(:instance |+1-1+N=N|)
			))))



(local (defthm group-operation-inverse-c
	 (implies (and (inv-c n a)
		       (inv-c n b)
		       (integerp n))
		  (equal (group-operation-c n
					    (inverse-c n a)
					    (inverse-c n b))
			 (inverse-c n (group-operation-c n b a))))))



(defthm group-operation-inverse-c-b
  (implies (and (inv-d n (cadr a))
		(inv-c (+ 1 n) (car a))
		(integerp n))
	   (EQUAL (GROUP-OPERATION-C N
                                   (inverse-C n
                                                (D-C (+ 1 N) (CAR A)))
                                   (inverse-C N  (PHI N (CADR A))))
                (inverse-C n
                            
                            (GROUP-OPERATION-C N (PHI N (CADR A))
                                               (D-C (+ 1 N) (CAR A))))))
   :hints (("Goal" :use ((:instance inv-phi-2 (a a))
			 (:instance inv-d-c-3 (a a))
			 (:instance group-operation-inverse-c
				   (a (D-C (+ 1 N) (CAR A)))
				   (b (PHI N (CADR A))))))))


(defthm group-operation-inverse-c-b-2
  (implies (and (inv-d n (cadr a))
		(inv-c (+ 1 n) (car a))
		(integerp n))
	   (EQUAL (GROUP-OPERATION-C N
                                   (INVERSE-C (+ -1 1 N)
                                              (D-C (+ 1 N) (CAR A)))
                                   (INVERSE-C N (PHI N (CADR A))))
                (INVERSE-C (+ 1 -1 N)
                           (GROUP-OPERATION-C N (PHI N (CADR A))
                                              (D-C (+ 1 N) (CAR A))))))
   :hints (("Goal" :in-theory (disable GROUP-OPERATION-INVERSE-C)
	    :use ((:instance -1+1+n=n)
			(:instance |+1-1+N=N|)
			(:instance group-operation-inverse-c-b)))))


(local (defthm d-c-d-c-+1+n-help
	 (implies (and (inv-c n a)
		       (integerp n))
		  (equal (D-C (+ -1 n) (D-C n a))
			 (ZERO-C (+ -1 -1 N))))))

(local (defthm |-1-1+1+N=-1+N|
	 (implies (integerp n)
		  (equal (+ -1 -1 1 n)
			 (+ -1 n)))
	 :rule-classes nil))

(local (defthm |+1-1-1+N=-1+N|
	 (implies (integerp n)
		  (equal (+ 1 -1 -1 n)
			 (+ -1 n)))
	 :rule-classes nil))


(local (defthm d-c-d-c-+1+n
	 (implies (and (inv-c (+ 1 N) a)
		       (integerp n))
		  (equal (D-C N (D-C (+ 1 N) a))
			 (ZERO-C (+ -1 N))))
	 :hints (("Goal" :use ((:instance |-1+1+N=N|)
			       (:instance |+1-1+N=N|)
			       (:instance |-1-1+1+N=-1+N|)
			       (:instance d-c-d-c-+1+n-help (n (+ 1 n)))
			       )))))

(local (defthm inv-phi-d-d
  (implies (and (inv-d n a) (integerp n))
	   (inv-c (+ n -1) (phi (+ n -1) (d-d n a))))
  :hints (("Goal" :in-theory (disable COMMUTATIVITY-OF-+)
	   :use ((:instance inv-phi (n (+ n -1))
				   (a (d-d n a))))))))


(local (defthm inv-phi-d-d-2
  (implies (and (inv-d n a) (integerp n))
	   (inv-c (+ -1 n) (phi (+ -1 n) (d-d n a))))
  :hints (("Goal" 
	   :use ((:instance inv-phi-d-d))))))


(local (defthm group-operation-zero-phi
	 (implies (and (inv-c (+ -1 n) a)
		       (integerp n))
		  (equal (group-operation-c (+ -1 n) 
					    (zero-c (+ -1 n))
					    a)
			 a))))




(local (defthm group-operation-d-phi-d-phi-help
	 (IMPLIES
    (AND (EQUAL (LIST (CAR A) (CADR A)) A)
         (INV-C (+ 1 N) (CAR A))
         (INV-D N (CADR A))
         (INTEGERP N))
    (EQUAL (GROUP-OPERATION-C (+ -1 N)
                              (D-C n
                                   (GROUP-OPERATION-C N (PHI N (CADR A))
                                                      (D-C (+ 1 N) (CAR A))))
                              (INVERSE-C (+ -1 N)
                                         (PHI (+ -1 N) (D-D N (CADR A)))))
           (ZERO-C (+ -1 N))))
))


(defthm group-operation-d-phi-d-phi
	 (IMPLIES
    (AND (EQUAL (LIST (CAR A) (CADR A)) A)
         (INV-C (+ 1 N) (CAR A))
         (INV-D N (CADR A))
         (INTEGERP N))
    (EQUAL (GROUP-OPERATION-C (+ -1 N)
                              (D-C (+ 1 -1 N)
                                   (GROUP-OPERATION-C N (PHI N (CADR A))
                                                      (D-C (+ 1 N) (CAR A))))
                              (INVERSE-C (+ -1 N)
                                         (PHI (+ -1 N) (D-D N (CADR A)))))
           (ZERO-C (+ 1 -1 -1 N))))
:hints (("Goal" :use ((:instance |+1-1+N=N|)
		      (:instance |+1-1-1+N=-1+N|)
		      (:instance group-operation-d-phi-d-phi-help))))
)

)


(check-chain-complex-p 
 (make-chain-complex :inv-ring 'inv-ring :addition-ring 'addition-ring :zero-element 'zero-element
		    :inverse 'inverse :product-ring 'product-ring :unit 'unit
		    :inv-cc 'inv-cone :group-operation-cc 'group-operation-cone :zero-cc 'zero-cone :external-cc 'external-cone
		    :inverse-cc 'inverse-cone :d-cc 'd-cone)
 'cone2-D-chi-C
)


;;;===========================================================================
;;;
;;; End of the cone construction
;;;
;;;===========================================================================



;;;----------------------------------------------------------------------------
;;; 
;;; Defining the generic theory:
;;;
;;;----------------------------------------------------------------------------


(include-book "generic-theory")


#|
(get-event-lst 
 '(inv-cone
   group-operation-cone
   zero-cone
   external-cone 
   inverse-cone
   d-cone
   |CONE2-D-CHI-C-is-a-chain-complex|
   )
 )
|#


(defconst *cone2*
  '((DEFUN INV-CONE (N A)
        (AND (EQUAL (LIST (CAR A) (CADR A)) A)
             (INV-C (1+ N) (CAR A))
             (INV-D N (CADR A))))
 (DEFUN GROUP-OPERATION-CONE (N A B)
        (LIST (GROUP-OPERATION-C (1+ N)
                                 (CAR A)
                                 (CAR B))
              (GROUP-OPERATION-D N (CADR A)
                                 (CADR B))))
 (DEFUN ZERO-CONE (N)
        (LIST (ZERO-C (1+ N)) (ZERO-D N)))
 (DEFUN EXTERNAL-CONE (N A B)
        (LIST (EXTERNAL-C (1+ N) A (CAR B))
              (EXTERNAL-D N A (CADR B))))
 (DEFUN INVERSE-CONE (N A)
        (LIST (INVERSE-C (1+ N) (CAR A))
              (INVERSE-D N (CADR A))))
 (DEFUN D-CONE (N A)
        (LIST (GROUP-OPERATION-C N (D-C (1+ N) (CAR A))
                                 (PHI N (CADR A)))
              (INVERSE-D (1- N) (D-D N (CADR A)))))
 (DEFTHM
  |CONE2-D-CHI-C-is-a-chain-complex|
  (AND
   (AND
    (AND
      (AND (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                              (INV-RING (ADDITION-RING X Y)))
                     (IMPLIES (AND (INV-RING X)
                                   (INV-RING Y)
                                   (INV-RING Z))
                              (EQUAL (ADDITION-RING (ADDITION-RING X Y) Z)
                                     (ADDITION-RING X (ADDITION-RING Y Z)))))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING (ZERO-ELEMENT) X)
                                X))
                (IMPLIES (INV-RING X)
                         (EQUAL (ADDITION-RING X (ZERO-ELEMENT))
                                X))
                (INV-RING (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING (INVERSE X) X)
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (EQUAL (ADDITION-RING X (INVERSE X))
                           (ZERO-ELEMENT)))
           (IMPLIES (INV-RING X)
                    (INV-RING (INVERSE X))))
      (AND (AND (IMPLIES (AND (INV-RING X) (INV-RING Y))
                         (INV-RING (PRODUCT-RING X Y)))
                (IMPLIES (AND (INV-RING X)
                              (INV-RING Y)
                              (INV-RING Z))
                         (EQUAL (PRODUCT-RING (PRODUCT-RING X Y) Z)
                                (PRODUCT-RING X (PRODUCT-RING Y Z)))))
           (IMPLIES (INV-RING X)
                    (EQUAL (PRODUCT-RING (UNIT) X) X))
           (IMPLIES (INV-RING X)
                    (EQUAL (PRODUCT-RING X (UNIT)) X))
           (INV-RING (UNIT)))
      (IMPLIES (AND (INV-RING X)
                    (INV-RING Y)
                    (INV-RING Z))
               (EQUAL (PRODUCT-RING X (ADDITION-RING Y Z))
                      (ADDITION-RING (PRODUCT-RING X Y)
                                     (PRODUCT-RING X Z))))
      (IMPLIES (AND (INV-RING X)
                    (INV-RING Y)
                    (INV-RING Z))
               (EQUAL (PRODUCT-RING (ADDITION-RING X Y) Z)
                      (ADDITION-RING (PRODUCT-RING X Z)
                                     (PRODUCT-RING Y Z)))))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-CONE N B)
                  (INTEGERP N))
             (INV-CONE N (GROUP-OPERATION-CONE N A B)))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-CONE N B)
                  (INV-CONE N C)
                  (INTEGERP N))
             (EQUAL (GROUP-OPERATION-CONE N (GROUP-OPERATION-CONE N A B)
                                          C)
                    (GROUP-OPERATION-CONE N A (GROUP-OPERATION-CONE N B C))))
    (INV-CONE N (ZERO-CONE N))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-RING R)
                  (INTEGERP N))
             (INV-CONE N (EXTERNAL-CONE N R A)))
    (IMPLIES (AND (INV-CONE N A) (INTEGERP N))
             (EQUAL (GROUP-OPERATION-CONE N A (ZERO-CONE N))
                    A))
    (IMPLIES (AND (INV-CONE N A) (INTEGERP N))
             (INV-CONE N (INVERSE-CONE N A)))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-CONE N B)
                  (INTEGERP N)
                  (EQUAL (GROUP-OPERATION-CONE N A B)
                         (ZERO-CONE N)))
             (EQUAL (INVERSE-CONE N A) B))
    (IMPLIES (AND (INV-CONE N A) (INTEGERP N))
             (EQUAL (GROUP-OPERATION-CONE N A (INVERSE-CONE N A))
                    (ZERO-CONE N)))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-CONE N B)
                  (INTEGERP N))
             (EQUAL (GROUP-OPERATION-CONE N A B)
                    (GROUP-OPERATION-CONE N B A)))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-CONE N B)
                  (INV-RING R)
                  (INTEGERP N))
             (EQUAL (EXTERNAL-CONE N R (GROUP-OPERATION-CONE N A B))
                    (GROUP-OPERATION-CONE N (EXTERNAL-CONE N R A)
                                          (EXTERNAL-CONE N R B))))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-RING S)
                  (INV-RING R)
                  (INTEGERP N))
             (EQUAL (EXTERNAL-CONE N (ADDITION-RING S R) A)
                    (GROUP-OPERATION-CONE N (EXTERNAL-CONE N S A)
                                          (EXTERNAL-CONE N R A))))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-RING S)
                  (INV-RING R)
                  (INTEGERP N))
             (EQUAL (EXTERNAL-CONE N (PRODUCT-RING S R) A)
                    (EXTERNAL-CONE N S (EXTERNAL-CONE N R A))))
    (IMPLIES (AND (INV-CONE N A) (INTEGERP N))
             (EQUAL (EXTERNAL-CONE N (UNIT) A) A))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-CONE N B)
                  (INTEGERP N))
             (EQUAL (INVERSE-CONE N (GROUP-OPERATION-CONE N A B))
                    (GROUP-OPERATION-CONE N (INVERSE-CONE N A)
                                          (INVERSE-CONE N B))))
    (IMPLIES (AND (INV-CONE N A)
                  (INV-RING S)
                  (INTEGERP N))
             (EQUAL (INVERSE-CONE N (EXTERNAL-CONE N S A))
                    (EXTERNAL-CONE N S (INVERSE-CONE N A))))
    (IMPLIES (INTEGERP N)
             (EQUAL (INVERSE-CONE N (ZERO-CONE N))
                    (ZERO-CONE N)))
    (IMPLIES (AND (INV-RING S) (INTEGERP N))
             (EQUAL (EXTERNAL-CONE N S (ZERO-CONE N))
                    (ZERO-CONE N))))
   (AND (AND (IMPLIES (AND (INV-CONE N A) (INTEGERP N))
                      (INV-CONE (+ N -1) (D-CONE N A)))
             (IMPLIES (AND (INV-CONE N A)
                           (INV-CONE N B)
                           (INTEGERP N))
                      (EQUAL (D-CONE N (GROUP-OPERATION-CONE N A B))
                             (GROUP-OPERATION-CONE (+ N -1)
                                                   (D-CONE N A)
                                                   (D-CONE N B))))
             (IMPLIES (AND (INV-CONE N A)
                           (INV-RING R)
                           (INTEGERP N))
                      (EQUAL (D-CONE N (EXTERNAL-CONE N R A))
                             (EXTERNAL-CONE (+ N -1)
                                            R (D-CONE N A))))
             (IMPLIES (INTEGERP N)
                      (EQUAL (D-CONE N (ZERO-CONE N))
                             (ZERO-CONE (+ N -1))))
             (IMPLIES (AND (INV-CONE N A) (INTEGERP N))
                      (EQUAL (D-CONE N (INVERSE-CONE N A))
                             (INVERSE-CONE (+ N -1) (D-CONE N A)))))
        (IMPLIES (AND (INV-CONE N A) (INTEGERP N))
                 (EQUAL (D-CONE (1- N) (D-CONE N A))
                        (ZERO-CONE (1- (1- N)))))))
  :HINTS
  (("Subgoal 24.2" :USE ((:INSTANCE GROUP-OPERATION-C-DISTRIVUTIVITY-CAR)))
   ("Subgoal 24.1" :USE ((:INSTANCE GROUP-OPERATION-D-DISTRIVUTIVITY
                                    (A (CADR A))
                                    (B (CADR B))
                                    (C (CADR C))))))))
)


(make-generic-theory *cone2*)